Pure Logic of Necessitation + L - Internet Explorer 2.0

Pure Logic of Necessitation + L
動機
	当たり前だが，Pure Logic of Necessitationの拡張として，証明可能性論理としては次の論理を考えたい．
		T. Kurahashi, Y. Sato; "The finite frame property of some extensions of the pure logic of necessitation"のFuture Worksとして挙げられている
		> In the context of provability logic, one may wonder the completeness of N+GL\mathsf{N + GL}N+GL（GL≡□(□φ→φ)→□φ\sf GL \equiv \Box(\Box\varphi \to \varphi) \to \Box\varphiGL≡□(□φ→φ)→□φ）, which is not of the form Accm,n\mathrm{Acc}_{m,n}Accm,n​ and thus not covered by this paper. Many of the N\sf NN counterpart of the famous extensions of K\sf KK are still left uninvestigated.

Def
	NL\sf NLNLは次の公理と推論規則を持つ．
	Axiom
		Taut\sf TautTaut: 命題論理のトートロジー全て
		L\sf LL: 様相論理の公理L: □(□φ→φ)→□φ\Box(\Box\varphi \to \varphi) \to \Box\varphi□(□φ→φ)→□φ
			形式化されたLöbの定理に対応．
	Rule
		モーダス・ポネンス: NL⊢φ\sf NL \vdash \varphiNL⊢φとNL⊢φ→ψ\sf NL \vdash \varphi \to \psiNL⊢φ→ψからNL⊢ψ\sf NL \vdash \psiNL⊢ψを導出
		ネセシテーション: NL⊢φ\sf NL \vdash \varphiNL⊢φからNL⊢□φ\sf NL \vdash \Box\varphiNL⊢□φを導出
			証明可能性述語についてT⊢φT \vdash \varphiT⊢φ  ⟹  \implies⟹T⊢PrT(⌜φ⌝‾)T \vdash \mathrm{Pr}_T (\overline{\ulcorner \varphi \urcorner})T⊢PrT​(┌φ┐​)に対応
				導出可能性条件D1．TTTはPA\sf PAPAのRE拡大